Issue998e.agda:7,3-4
Set (lsuc ℓ₁) is not less or equal than Set (lsuc ℓ)
when checking that the type (ℓ₁ : Level) → Set ℓ₁ → D of the
constructor c fits in the sort Set (lsuc ℓ) of the datatype.
